(set-logic QF_FP)
(set-option :incremental true)
(set-option :produce-models true)

(declare-const a Float32)
(declare-const b Float32)
(declare-const c Float32)
(declare-const d Float32)
(declare-const e Float32)

(echo "Show that fused multiplication and addition (fp.fma RM a b c) is")
(echo "different from (fp.add RM (fp.mul RM a b) c)")
(push 1)
(declare-const rm RoundingMode)
(assert (distinct (fp.fma rm a b c) (fp.add rm (fp.mul rm a b) c)))
(echo "Expect sat")
(check-sat)
(echo "Value of `a`:")
(get-value (a))
(echo "Value of `b`:")
(get-value (b))
(echo "Value of `c`:")
(get-value (c))
(echo "Value of `RM`:")
(get-value (rm))
(echo "Value of `(fp.fma RM a b c)`:")
(get-value ((fp.fma rm a b c)))
(echo "Value of `(fp.add RM (fp.mul RM a b) c))`:")
(get-value ((fp.add rm (fp.mul rm a b) c)))
(pop 1)

(echo "Show that floating-point addition is not associative:")
(echo "(a + (b + c)) != ((a + b) + c)")
(push 1)
(assert (distinct (fp.add RNE a (fp.add RNE b c)) (fp.add RNE (fp.add RNE a b) c)))
(echo "Expect sat")
(check-sat)
(echo "Value of `a`:")
(get-value (a))
(echo "Value of `b`:")
(get-value (b))
(echo "Value of `c`:")
(get-value (c))
(pop 1)

(echo "Restrict `a` to be either NaN or positive infinity:")
(push 1)
(assert (or (= a (_ +oo 8 24)) (= a (_ NaN 8 24))))
(echo "Expect sat")
(check-sat)
(get-value (a b c))
(pop 1)

(echo "Find normal FP number that rounds to different integer values for different rounding modes:")
(push 1)
(assert (fp.isNormal d))
(assert (distinct ((_ fp.to_ubv 16) RTP d) ((_ fp.to_ubv 16) RTN d)))
(echo "Expect sat")
(check-sat)

(echo "Value of `d`:")
(get-value (d))
(echo "Value of `((_ fp.to_ubv 16) RTP d)`:")
(get-value (((_ fp.to_ubv 16) RTP d)))
(echo "Value of `((_ fp.to_ubv 16) RTN d)`:")
(get-value (((_ fp.to_ubv 16) RTN d)))
(echo "Value of `d` as a rational:")
(get-value ((fp.to_real d)))
(pop 1)

(echo "Find FP number between +zero and the smallest positive FP number:")
(push 1)
(assert (and (fp.lt (_ +zero 8 24) e) (fp.lt e ((_ to_fp 8 24) (_ bv1 32)))))

(echo "Expect unsat")
(check-sat)
(pop 1)
